\subsection{Background}
Background from Yves about ACL models here\ldots we need to put some related
work here!!!

\subsection{Problem Statement}

The access control is becoming a mandatory feature for most systems (e.g.
information systems, service-based architectures), due to the importance of
preserving confidentiality and safety both of clients and of the application
itself. Many models exist to express such policies (e.g. RBAC,
OrBAC~\cite{citeulike:1362491}) in a simple and intuitive way. These access
control description formalisms are typically built for enabling the modification
of the access control policy over time. On the other hand, as the access control
dimension typically changes during the system's lifetime, the system itself also
evolves leading to changes of its functionalities and overall behavior. To
express the behaviour of a system, several formalisms are currently heavily used
in the industry, e.g. UML statecharts or BPEL. If we combine in the
same model a system's behavior together with the access control concern, we
obtain a model which is enforcing an access control policy. In this scenario of
system development, which is similar to the one described
in~\cite{Ray04anaspect-based}, the access control concern is pervasive across
the model.

In this paper we will focus on the co-evolution of an access control policy --
expressing permissions and prohibitions about users accessing certain resources
in the application -- and the functional description of the application. We
consider models which simultaneously include function and the implementation of
an access control policy and propose a methodology that allows these two
dimensions to evolve in a non-conflicting fashion. This means that, when a
change is made such that a new access control permission/prohibition is
enforced: 1) we want to make sure that the access control policies enforced are
not disabled, or become stricter; 2) previously implemented functionalities are
still in place. On the other hand, when a new functionality is added, we want to
be sure that 1) and 2) above also still hold. As a preliminary disclaimer, for
the time being we are dealing with \emph{monotonic} evolution, in the sense that
the permissions/prohibitions can only added, but not modified. The same is
assumed for the functionality dimension. This is not detrimental to our results,
as this study can be used as a basis to develop \emph{non-monotonic} evolution.

In the following sections we will describe a methodology that allows the
incremental evolution of the functional and access control concerns in an
intergated model. In order to do so we will use safe mechanisms based on formal
proofs and model checking to guarantee that previously modeled access control
permissions/prohibitions and functionalities are not invalidated as the system
evolves. In order to profit from existing theoretical results we use algebraic
Petri nets~\cite{Rei91} as our integrated models. This is done without loss of
generality regarding more standard behavioral description formalisms such as
statecharts. In particular, we have presented in~\cite{LucQinSouTej:11} a
partially bidirectional transformation of statecharts into algebraic Petri nets.

The paper is organized as follows: in section~\ref{sec:models_acp} we lay the
foundations of our approach by describing the hypothesis of our work and in
particular how behavior and access control concerns are represented in an
algebraic Petri net; in section~\ref{sec:safe_co_evolution} we explain the
formal principles of our co-evolution methodology;
section~\ref{sec:experimentation} demonstrates the applicability of our
methodology by providing extracts of an example where a library management
system (LMS) evolves both in the access control and the functional dimensions;
finally section~\ref{sec:discussion} provides a discussion of the presented work
and section~\ref{sec:conclusion} concludes.
